es:event_system{i:l}, L:(Id List), e:es-E(es).
fischer{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2}
fischer(es; L)
 (loc(e)  L)
 (es-when(es; mkid{x:ut2}; e) = mkid{taken:ut2}  Id)
 ((es-after(es; mkid{x:ut2}; e) = mkid{taken:ut2}  Id))
 guard(((es-after(es; mkid{x:ut2}; e) = mkid{free:ut2}  Id)
 guard( ((es-isrcv(es; e))
 guard( c (((es-tag(es; e) = mkid{free:ut2}  Id)
 guard( c  (i:Id
 guard( c  (((i  L)  ((i = loc(e)))  (es-lnk(es; e) = <i, loc(e), mkid{z:ut2}>  IdLnk))))
 guard( c  f-newround{x:ut2, free:ut2, mine:ut2}
 guard( c  f-newround(es; L; es-sender(es; e)))))) 

latex

Definitions	if b then t else f fi , ff, eq_atom{$n:n}(x; y), atom2-deq, id-deq, t.1, eqof(d), eq_id(a; b), P  Q, prop{i:l}, sq_type(T), t  T, P  Q, @e(xv), b, A c B, P  Q, guard(T), A, mkid{$x:ut2}, P  Q, Id, x:A. B(x), False, l_all(L; T; x.P(x)), P  Q, es-dtype(es; i; x; T), x:A. B(x), (x  l), fischer
Lemmas	event system wf, es-E wf, fischer wf, es-loc wf, Id wf, l member wf, es-when wf, es-after wf, not wf, false wf, assert-eq-id, eq id wf, assert wf, not functionality wrt iff, Id sq